#include "aigCircuit.h"
#include "base/aig.h"
#include <cstring>
#include <limits.h>

using QuteRSAT::AigCircuit;

void AigCircuit::transform( StrashAIG & ckt , vector<AigIndex> & index )
{
   unsigned * focnt   = new unsigned [_nodes.size()];
   unsigned * trav    = new unsigned [_nodes.size()];
   AigLit   * mapping = new AigLit   [_nodes.size()];
   mapping[0]=0;
   
   memset( focnt , 0 , sizeof( unsigned ) * _nodes.size() );

   for( unsigned i = 0 ; i < _nodes.size() ; ++i )
   {
      if( ! _nodes[i].isPi() ) 
      {
         focnt[ _nodes[i]._fanin[0]._index ] +=1; 
         focnt[ _nodes[i]._fanin[1]._index ] +=1; 
      }
   }
   for( unsigned i = 0 ; i < _piList.size() ; ++i )
      focnt[ _piList[i]._index ] +=1;
   focnt[0] +=1;

   unsigned ptr = 0;

   for( unsigned i = 0 ; i < _nodes.size() ; ++ i) 
      if( focnt[ i ] == 0 ) 
         trav[ ptr ++ ] = i ;
      
   unsigned idx = 0;
   while( idx != ptr )
   {
      unsigned x = trav[ idx++ ];
      assert( ! _nodes[x].isPi() );
      for( int i = 0 ; i < 2 ; ++ i )
      {
         unsigned n = _nodes[x]._fanin[i]._index ;
         focnt[n] -=1;
         if( focnt[n] == 0 )
            trav[ ptr ++ ] = n ;
      }
   }
   for( unsigned i = 0 ; i < _piList.size() ; ++i )
   {
      unsigned n = _piList[i]._index;
      focnt[n]-=1;
      assert( focnt[n] == 0 );
      trav[ ptr ++ ] = n;
   }
   for( int i = ptr -1 ; i >= 0 ; -- i)
   {
      unsigned n = trav[i];
      assert( focnt[n] == 0 );
      if( n == 0 ){ assert( false );}
      AigNode node = _nodes[ n ];

      if( _nodes[n].isPi() )
      {
         mapping[n] = toAigLit( ckt.size() , 0 );
         ckt.createBase();
      }
      else 
      {
         AigLit v[2] ;
         for( int j = 0 ; j < 2 ; ++ j )
         {
            AigLit m = mapping[ node._fanin[j]._index ];
            v[j] = toAigLit( var(m) , sign(m)^node._fanin[j]._sign );
         }
         mapping[n] = ckt.createAND( v[0] , v[1] );
         assert( var(mapping[n]) == ckt.sz-1 );
      }
   }
   for( unsigned i = 0 ; i < _poList.size() ; ++ i)
   {
      AigLit m = mapping[ _poList[i]._index ];
      ckt._po.push( toAigLit( var(m) , sign(m)^_poList[i]._sign ) );
   }
   ckt._andFlag = ckt._ppiFlag = ckt.size() - ckt.andSize();

   for( unsigned i = 0 ; i < index.size() ; ++ i )
   {
      AigIndex x = index[i];
      if( x._data != UINT_MAX )
         index[i] = AigIndex( var(mapping[x._index]) , sign(mapping[x._index]) ^ x._sign );
   }

   delete [] focnt;
   delete [] trav;
   delete [] mapping;
}

